Safety inspection of software specifications and automatic synthesis of software.
Keywords: specifications, verification, software, automatic synthesis, safety
Software that serves as social infrastructure, such as airplane control programs and bank ATMs, is a system that provides services while interacting with users. Such systems are called reactive systems. The design specifications, which serve as blueprints for building and verifying reactive systems, are crucial. By verifying whether the software operates according to the specifications, we ensure the safety of the software. However, if there are deficiencies or inconsistencies in the specifications themselves, the verification becomes pointless. Therefore, research is being conducted to investigate whether there are any errors in the specifications themselves. In particular, when various requirements for different software are included in the specifications, it is possible that the software does not exist. Thus, research is also being conducted to determine whether software that operates according to the specifications exists. As a development of this, research is also being conducted on the automatic synthesis of software from specifications. By automating the synthesis, we can efficiently create safe software.
- Company：埼玉大学 オープンイノベーションセンター
- Price：Other
